﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace Logic
{
	class CNFSentence : ICloneable
    {
        public LogicalSystem LogicalSystem;
        public List<List<int>> Formula;
		public bool? AlwaysTrueOrFalse = null;
		public Dictionary<int, VarInclusionInfo> VariableIndex;       
	

		private CNFSentence()
		{
            
		}

		public CNFSentence(LogicalSystem ls)
		{
			LogicalSystem = ls;
			AlwaysTrueOrFalse = true;
			Formula = new List<List<int>>();
            VariableIndex = new Dictionary<int, VarInclusionInfo>();
		}

        public CNFSentence(LogicalSystem ls, List<List<int>> formula)
        {
            this.LogicalSystem = ls;
            this.Formula = formula;
            VariableIndex = new Dictionary<int, VarInclusionInfo>();
        }

        

        public override string ToString()
        {
			if (AlwaysTrueOrFalse != null) return "Always " + AlwaysTrueOrFalse.Value;

            StringBuilder sb = new StringBuilder();
            foreach (var t in Formula)
            {
                foreach (var v in t)
                {
                    int val = v;
                    if (val < 0)
                    {
                        sb.Append('~');
                        val = ~val;
                    }

                    sb.Append(LogicalSystem.Symbols[val]);
                    sb.Append(' ');
                }
                sb.AppendLine();
            }

            return sb.ToString();
        }

		public object Clone()
		{
			CNFSentence clone = new CNFSentence();
			clone.LogicalSystem = LogicalSystem;
			if (AlwaysTrueOrFalse == true) { clone.AlwaysTrueOrFalse = true; clone.Formula = new List<List<int>>(); return clone; }
			if (AlwaysTrueOrFalse == false) { clone.AlwaysTrueOrFalse = false; return clone; }

			clone.Formula = new List<List<int>>(Formula.Select(x => new List<int>(x)).ToList());
			if (this.VariableIndex != null)
			{
				clone.VariableIndex = new Dictionary<int, VarInclusionInfo>();
				foreach (KeyValuePair<int, VarInclusionInfo> kvp in VariableIndex)
					clone.VariableIndex.Add(kvp.Key, kvp.Value.Clone());
			}
			return clone;
		}

		/// <summary>
		/// Sorts every clause then
		/// removes dublicates of a symbol in a clause (A | A == A),
		/// and removes clauses, that contain A | ~A and therefore are true.        
		/// </summary>
        public void Clean()
        {
			if (AlwaysTrueOrFalse != null) return;
            for (int i = 0; i < Formula.Count; i++)
            {
                List<int> clause = Formula[i];
				clause.Sort(new Comparison<int>(SymbolOrderComparison));
				
				bool istrue = false;
				for (int j = 0; j < clause.Count-1; j++)
				{
					if (clause[j] == clause[j + 1])
					{
						clause.RemoveAt(j);
						j--;
						continue;
					}
					if (clause[j] == ~clause[j+1])
					{
						istrue = true;
						break;
					}					
				}

                if (istrue)	
                {
                    Formula.RemoveAt(i);
                    i--;
                }
            }

			if (Formula.Count == 0)
			{
				AlwaysTrueOrFalse = true;
				Formula.Clear();
			}
        }
      
        /// <summary>
        /// Tries to compact CNF expression by using following rules:
        /// 1. A & A == A
        /// 2. A & ~A == False
        /// 3. A & (A | B) == A
        /// 4. A & (~A | B) == A & B
        /// 5. (A | B) & (A | ~B) == A
        /// </summary>
        public void Compact()
        {			
            Clean();
			if (AlwaysTrueOrFalse != null) return;

			int simplificationsMade;

			do
			{
				simplificationsMade = 0;
				List<int> removedClausesIndexes = new List<int>();

				//BUGGED in RemoveAt(i); i--;
				for (int i = 0; i < Formula.Count - 1; i++)
				{
					for (int j = i + 1; j < Formula.Count; j++)
					{
						List<int> c1 = Formula[i];
						List<int> c2 = Formula[j];
						bool reversedComp = false;
						if (c1.Count > c2.Count) { var tmp = c1; c1 = c2; c2 = tmp; reversedComp = true; }
						int i1 = 0, i2 = 0;
						int? negativeSymbolIndexIn2 = null;
						bool fail = false;
						for (; i1 < c1.Count; i2++)
						{
							if (i2 == c2.Count) { fail = true; break; }
							if (c1[i1] == c2[i2]) { i1++; continue; }
							if (c1[i1] == ~c2[i2]) { if (negativeSymbolIndexIn2 != null) { fail = true; break; } else { negativeSymbolIndexIn2 = i2; i1++; } }

						}

						if (!fail)
						{
							if (negativeSymbolIndexIn2 == null) //Rules 1,3
							{
								if (reversedComp) { removedClausesIndexes.Add(i); } else { removedClausesIndexes.Add(j); }
								simplificationsMade++;
								continue;
							}
							if (c1.Count == c2.Count)
							{
								if (c1.Count == 1) //Rule 2
								{
									AlwaysTrueOrFalse = false;
									Formula = null;
									return;
								}
								else //Rule 5
								{
									if (reversedComp) { removedClausesIndexes.Add(j); } else { removedClausesIndexes.Add(i); }
									c2.RemoveAt(negativeSymbolIndexIn2.Value);
									simplificationsMade++;
								}
							}
							else if (c1.Count == 1) //Rule 4
							{
								c2.RemoveAt(negativeSymbolIndexIn2.Value);
								simplificationsMade++;
							}
						}
					}
				}

				removedClausesIndexes = removedClausesIndexes.Distinct().OrderByDescending(x => x).ToList();
				foreach (int ri in removedClausesIndexes)
					Formula.RemoveAt(ri);

			} while (simplificationsMade > 0);
        }

        int ClauseLengthComparison(List<int> c1, List<int> c2)
        {
            return c1.Count < c2.Count ? -1 : (c1.Count == c2.Count ? 0 : 1);
        }

		int SymbolOrderComparison(int id1, int id2)
		{
			if (id1 < 0) id1 = ~id1;
			if (id2 < 0) id2 = ~id2;

			return id1 < id2 ? -1 : (id1 == id2 ? 0 : 1);
		}

		public static CNFSentence FromTruthTable(LogicalSystem ls, Func<int[], bool> func, int nvars)
		{
			Random rand = new Random();
			return new CNFSentence(ls, ConstructCNF(func, new int[nvars], rand));
		}

        static List<List<int>> ConstructCNF(Func<int[], bool> func, int[] assigned, Random rand)
        {
			List<List<int>> formula = new List<List<int>>();
			int[] apass = (int[])assigned.Clone();

			List<int> unassignedIndexes = new List<int>(apass.Length);
			for (int i = 0; i < apass.Length; i++)
				if (apass[i] == 0) unassignedIndexes.Add(i);

			//We split hypercube randomly for simplicity. Later - need to measure subcubes difference for each, and choose minimal.
			int varIndex = unassignedIndexes[rand.Next(unassignedIndexes.Count)];		
			
			//assigned Variable True Function True etc.
			int vtft = 0, vtff = 0, vfft = 0, vfff = 0;
			for (int i = 0; i < unassignedIndexes.Count; i++) apass[unassignedIndexes[i]] = -1;

			int j = 0;
			for (;j < unassignedIndexes.Count;)
			{
				for (j = 0; j < unassignedIndexes.Count; j++)
				{
					int ci = unassignedIndexes[j];
					if (apass[ci] == -1) {apass[ci] = 1;	break; }
					else {apass[ci] = -1; continue;	}
				}

				//we consider ~Func for CNF, not DNF
				bool result = !func(apass);

				if (apass[varIndex] == 1)
				{
					if (result) vtft++; else vtff++;
				}
				else
				{
					if (result) vfft++; else vfff++;
				}
			}

			if (vtft > 0)
			{
				if (vtff == 0)
					formula.Add(new List<int>(new[] { ~varIndex }));
				else
				{
					int[] at = (int[])assigned.Clone();
					at[varIndex] = 1;
					List<List<int>> r = ConstructCNF(func, at, rand);
					foreach (List<int> l in r)
					{
						l.Add(~varIndex);
						formula.Add(l);
					}
				}				
			}

			if (vfft > 0)
			{
				if (vfff == 0)
					formula.Add(new List<int>(new[] { varIndex }));
				else
				{
					int[] af = (int[])assigned.Clone();
					af[varIndex] = -1;
					List<List<int>> r = ConstructCNF(func, af, rand);
					foreach (List<int> l in r)
					{
						l.Add(varIndex);
						formula.Add(l);
					}
				}
			}

			return formula;
        }

		public bool Evaluate(int[] assigment)
		{
			if (AlwaysTrueOrFalse != null) return AlwaysTrueOrFalse.Value;

			for (int i = 0; i < Formula.Count; i++)
			{
				List<int> clause = Formula[i];
				bool istrue = false;
				for (int j = 0; j < clause.Count; j++)
				{
					int literal = clause[j];
					bool neg = false;
					if (literal < 0)
					{
						neg = true;
						literal = ~literal;
					}

					int val = assigment[literal];
					if (val == 1 && !neg || val == -1 && neg)
					{
						istrue = true;
						break;
					}
				}

				if (!istrue)
					return false;
			}

			return true;
		}

		public bool IsEquivalentTo(CNFSentence cnf)
		{
			if (cnf.LogicalSystem != this.LogicalSystem) throw new Exception("Variable sets differ");	
			

			int[] a = new int[this.LogicalSystem.Symbols.Count];
			for (int j = 0; j < a.Length; j++) a[j] = -1;

			int i = 0;
			for (; i < a.Length; )
			{
				for (i = 0; i < a.Length; i++)
				{
					if (a[i] == -1) { a[i] = 1; break; }
					else { a[i] = -1; continue; }
				}

				if (Evaluate(a) != cnf.Evaluate(a)) return false;
			}

			return true;
		}

		public void ChangeVariableSet(LogicalSystem newVs, List<Tuple<int,int>> corresp)
		{
			LogicalSystem = newVs;
			if(AlwaysTrueOrFalse != null) return;
			foreach (List<int> cl in Formula)
			{
				for (int i = 0; i < cl.Count; i++)
				{
					foreach (Tuple<int,int> cor in corresp)
					{
						if (cl[i] == cor.Item1)
						{
							cl[i] = cor.Item2;
							break;
						}
						else if (cl[i] == ~cor.Item1)
						{
							cl[i] = ~cor.Item2;
							break;
						}
					}						
				}				
			}
		}

		public void Append(CNFSentence add)
		{
			if (AlwaysTrueOrFalse == false) return;
			if (AlwaysTrueOrFalse == true) AlwaysTrueOrFalse = null;
			this.Formula.AddRange(add.Formula.Select(x => new List<int>(x)).ToList());			
		}

		public void AppendClause(List<int> cl)
		{
			if (AlwaysTrueOrFalse == false) return;
			if (AlwaysTrueOrFalse == true) AlwaysTrueOrFalse = null;
			this.Formula.Add(new List<int>(cl));

            foreach (int v in cl)
            {
                bool neg = false;
                //TODO: what should I do with this appearing everywhere??
                int av = v; if (av < 0) { av = ~av; neg = true; }
                VarInclusionInfo info;

                if (!VariableIndex.TryGetValue(av, out info))
                {
                    info = new VarInclusionInfo();
                    VariableIndex.Add(av, info);
                }
                info.ClausesIn.Add(this.Formula.Count - 1);
                if (neg)
                    info.NegInclusions++;
                else
                    info.PosInlusions++;
            }
		}

		public void BuildIndex()
		{
            if(AlwaysTrueOrFalse != null) return;
			VariableIndex = new Dictionary<int, VarInclusionInfo>();
            for (int i = 0; i < Formula.Count; i++)
            {
				List<int> cl = Formula[i];
				for (int j = 0; j < cl.Count; j++)
				{
					int v = cl[j]; bool neg = false;					
					if (v < 0) { v = ~v; neg = true; }
					VarInclusionInfo info;
					if (!VariableIndex.TryGetValue(v, out info))
					{
						info = new VarInclusionInfo();
						VariableIndex.Add(v, info);
					}

					info.ClausesIn.Add(i);
					if (neg)
						info.NegInclusions++;
					else
						info.PosInlusions++;
				}
            }
		}

		public class VarInclusionInfo
		{
			public List<int> ClausesIn = new List<int>();
			public int PosInlusions, NegInclusions;

			public VarInclusionInfo Clone()
			{
				return new VarInclusionInfo()
				{
					 ClausesIn = new List<int>(this.ClausesIn),
					 PosInlusions = this.PosInlusions,
					 NegInclusions = this.NegInclusions
				};
			}
		}
	}
}
